perm filename PROOFS[F80,JMC]1 blob
sn#547743 filedate 1980-11-24 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 <LISP>LISP.SAV133
C00040 ENDMK
C⊗;
<LISP>LISP.SAV;133
<BOYER>CODE.;1
<BOYER>CODE1.;781
<BOYER>DATA.;1
<BOYER>DATA1.;2
Thursday, November 20, 1980 4:11PM-PST!
←DEFN(NTH (U N)
(IF (ZEROP N)
U
(IF (EQUAL N 1)
(CAR U)
(NTH (CDR U) (SUB1 N)))))
The lemma SUB1.LESSP informs us that (COUNT N)
decreases according to the well-founded function LESSP in
each recursive call. Hence, NTH is accepted under the
definitional principle.
[3739 cns / 13.3 s + 0.0 gc + .6 io (= 16 @ 1)]
NTH
!
←DEFN(INDEX (U X)
(IF (NLISTP U)
0
(IF (EQUAL (CAR U) X)
1
(ADD1 (INDEX (CDR U) X)))))
The lemma CDR.LESSP can be used to prove that
(COUNT U) decreases according to the well-founded function
LESSP in each recursive call. Hence, INDEX is accepted
under the definitional principle. Observe that
(NUMBERP (INDEX U X)) is a theorem.
[1767 cns / 6.4 s + 0.0 gc + .7 io (= 9 @ 1)]
INDEX
!
←DEFN(MEMB (X Y)
(IF (NLISTP Y)
(FALSE)
(IF (EQUAL X (CAR Y))
T
(MEMB X (CDR Y)))))
The lemma CDR.LESSP informs us that (COUNT Y) goes
down according to the well-founded function LESSP in each
recursive call. Hence, MEMB is accepted under the
definitional principle. Note that:
(OR (FALSEP (MEMB X Y))
(TRUEP (MEMB X Y)))
is a theorem.
[1715 cns / 6.3 s + 0.0 gc + .6 io (= 7 @ 1)]
MEMB
!
←PROVE.LEMMA(FOO (REWRITE)
(IMPLIES (MEMB X U)
(EQUAL (NTH U (INDEX U X)) X)))
This conjecture can be simplified, using the abbreviation
IMPLIES, to:
(IMPLIES (MEMB X U)
(EQUAL (NTH U (INDEX U X)) X)),
which we will name *1.
We will appeal to induction. Two inductions are
suggested by terms in the conjecture. However, they merge
into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP U)) (p U X))
(IMPLIES (AND (LISTP U) (p (CDR U) X))
(p U X))).
The inequality CDR.LESSP establishes that the measure
(COUNT U) decreases according to the well-founded function
LESSP in the induction step of the scheme. The above
induction scheme produces the following three new
conjectures:
Case 3. (IMPLIES (AND (NOT (LISTP U)) (MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)).
This simplifies, expanding the definitions of NLISTP,
INDEX, EQUAL, NTH, and MEMB, to:
T.
Case 2. (IMPLIES (AND (LISTP U)
(NOT (MEMB X (CDR U)))
(MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)),
which we simplify, unfolding NLISTP, INDEX, and MEMB, to:
(IMPLIES (AND (LISTP U)
(NOT (MEMB X (CDR U)))
(EQUAL (CAR U) X))
(EQUAL (NTH U 1) X)).
However this simplifies again, expanding NUMBERP, EQUAL,
and NTH, to:
T.
Case 1. (IMPLIES (AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(MEMB X U))
(EQUAL (NTH U (INDEX U X)) X)),
which simplifies, expanding the definitions of NLISTP,
INDEX, and MEMB, to two new formulas:
Case 1.2.
(IMPLIES
(AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(MEMB X (CDR U))
(NOT (EQUAL (CAR U) X)))
(EQUAL (NTH U (ADD1 (INDEX (CDR U) X)))
X)),
which we again simplify, applying SUB1.ADD1 and
ADD1.EQUAL, and opening up the definitions of NUMBERP
and NTH, to:
(IMPLIES (AND (LISTP U)
(EQUAL (CDR U) X)
(MEMB X (CDR U))
(NOT (EQUAL (CAR U) X)))
(NOT (EQUAL (INDEX (CDR U) X) 0))),
which we again simplify, clearly, to:
(IMPLIES
(AND (LISTP U)
(MEMB (CDR U) (CDR U))
(NOT (EQUAL (CAR U) (CDR U))))
(NOT (EQUAL (INDEX (CDR U) (CDR U)) 0))).
Appealing to the lemma CAR/CDR.ELIM, we now replace U
by (CONS V Z) to eliminate (CDR U) and (CAR U). The
result is:
(IMPLIES (AND (MEMB Z Z) (NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
Name the above subgoal *1.1.
Case 1.1.
(IMPLIES
(AND (LISTP U)
(EQUAL (NTH (CDR U) (INDEX (CDR U) X))
X)
(EQUAL (CAR U) X))
(EQUAL (NTH U 1) X)),
which we again simplify, opening up NUMBERP, EQUAL, and
NTH, to:
T.
So we now return to:
(IMPLIES (AND (MEMB Z Z) (NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we named *1.1 above. Let us appeal to the induction
principle. There are two plausible inductions. However,
they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p Z V))
(IMPLIES (AND (LISTP Z) (p (CDR Z) V))
(p Z V))).
The inequality CDR.LESSP establishes that the measure
(COUNT Z) decreases according to the well-founded function
LESSP in the induction step of the scheme. The above
induction scheme generates four new goals:
Case 4. (IMPLIES (AND (NOT (LISTP Z))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we simplify, expanding the definitions of NLISTP,
INDEX, EQUAL, and MEMB, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
This simplifies, expanding NLISTP, INDEX, and MEMB, to
two new goals:
Case 3.2.
(IMPLIES
(AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(MEMB Z (CDR Z))
(NOT (EQUAL V Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))),
which we again simplify, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP Z)
(NOT (MEMB (CDR Z) (CDR Z)))
(NOT (EQUAL V Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))).
However this again simplifies, using linear arithmetic,
to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(EQUAL V (CDR Z))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))),
which we simplify, unfolding NLISTP, INDEX, and MEMB, to
two new conjectures:
Case 2.2.
(IMPLIES
(AND (LISTP Z)
(MEMB Z (CDR Z))
(NOT (EQUAL (CDR Z) Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))).
However this again simplifies, using linear arithmetic,
to:
T.
Case 2.1.
(IMPLIES (AND (LISTP Z)
(NOT (EQUAL (CDR Z) Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))),
which we again simplify, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(MEMB Z Z)
(NOT (EQUAL V Z)))
(NOT (EQUAL (INDEX Z Z) 0))).
This simplifies, unfolding the definitions of NLISTP,
INDEX, and MEMB, to the following two new formulas:
Case 1.2.
(IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(MEMB Z (CDR Z))
(NOT (EQUAL V Z))
(NOT (EQUAL (CAR Z) Z)))
(NOT (EQUAL (ADD1 (INDEX (CDR Z) Z)) 0))).
This simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND (LISTP Z)
(NOT (EQUAL (INDEX (CDR Z) (CDR Z)) 0))
(NOT (EQUAL V Z))
(EQUAL (CAR Z) Z))
(NOT (EQUAL 1 0))).
However this simplifies again, using linear arithmetic,
to:
T.
That finishes the proof of *1.1, which also finishes
the proof of *1. Q.E.D.
[11248 cns / 61.9 s + 0.0 gc + 13.7 io (= 77 @ 1)]
FOO
!
←DEFN(ISPERM (U)
(IF (NLISTP U)
T
(AND (NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U)))))
The lemma CDR.LESSP can be used to prove that
(COUNT U) decreases according to the well-founded function
LESSP in each recursive call. Hence, ISPERM is accepted
under the definitional principle. From the definition we
can conclude that:
(OR (FALSEP (ISPERM U))
(TRUEP (ISPERM U)))
is a theorem.
[2351 cns / 7.8 s + 0.0 gc + .8 io (= 9 @ 1)]
ISPERM
!
←DEFN(LEN (X)
(IF (NLISTP X)
0
(ADD1 (LEN (CDR X)))))
The lemma CDR.LESSP can be used to show that (COUNT X)
decreases according to the well-founded function LESSP in
each recursive call. Hence, LEN is accepted under the
principle of definition. From the definition we can
conclude that (NUMBERP (LEN X)) is a theorem.
[978 cns / 4.1 s + 0.0 gc + .6 io (= 5 @ 1)]
LEN
!
←PROVE.LEMMA(FOO2 (REWRITE)
(IMPLIES (AND (NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)))
This formula can be simplified, using the abbreviations NOT,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we will name *1.
Let us appeal to the induction principle. Five
inductions are suggested by terms in the conjecture.
However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP N)) (p U N))
(IMPLIES (EQUAL N 0) (p U N))
(IMPLIES (AND (NUMBERP N)
(NOT (EQUAL N 0))
(p (CDR U) (SUB1 N)))
(p U N))).
The inequality SUB1.LESSP establishes that the measure
(COUNT N) decreases according to the well-founded function
LESSP in the induction step of the scheme. Note, however,
the inductive instance chosen for U. The above induction
scheme generates the following four new goals:
Case 4. (IMPLIES (AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)).
This simplifies, applying CDR.NLISTP, and expanding the
definitions of NTH, NLISTP, ISPERM, LENGTH, EQUAL, and
LESSP, to four new conjectures:
Case 4.4.
(IMPLIES (AND (NOT (EQUAL (SUB1 N) 0))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)).
But this again simplifies, using linear arithmetic, to:
T.
Case 4.3.
(IMPLIES
(AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)),
which we again simplify, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL (SUB1 N) 0))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)).
However this again simplifies, using linear arithmetic,
to:
T.
Case 4.1.
(IMPLIES
(AND (LESSP (LENGTH (CDR U)) (SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)),
which we again simplify, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (ISPERM (CDR U)))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we simplify, expanding NLISTP, INDEX, ISPERM,
LENGTH, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (EQUAL (SUB1 N) 0)
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)).
Appealing to the lemma SUB1.ELIM, replace N by (ADD1 X)
to eliminate (SUB1 N). We use the type restriction lemma
noted when SUB1 was introduced to constrain the new
variable. We would thus like to prove:
(IMPLIES (AND (NUMBERP X)
(EQUAL X 0)
(NOT (LESSP (LENGTH U) (ADD1 X)))
(ISPERM U)
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (INDEX U (NTH U (ADD1 X)))
(ADD1 X))),
which we simplify, opening up the functions NUMBERP,
EQUAL, NTH, NLISTP, INDEX, ISPERM, LENGTH, and LESSP, to:
(IMPLIES (AND (NOT (LESSP (LENGTH U) 1))
(ISPERM U))
(EQUAL 1 1)).
This simplifies again, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH U) N))
(ISPERM U)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (INDEX U (NTH U N)) N)),
which we simplify, applying the lemma CDR.NLISTP, and
opening up the functions NTH, NLISTP, ISPERM, LENGTH,
EQUAL, LESSP, and INDEX, to four new conjectures:
Case 1.4.
(IMPLIES (AND (EQUAL 0 (SUB1 N))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (INDEX U (NTH (CDR U) (SUB1 N)))
N)).
But this again simplifies, applying SUB1.ADD1, and
opening up the definitions of NLISTP, INDEX, and LESSP,
to the following two new goals:
Case 1.3.2.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (LENGTH (CDR U)) (SUB1 N)))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(EQUAL (ADD1 (INDEX (CDR U)
(NTH (CDR U) (SUB1 N))))
N)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.1.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (LENGTH (CDR U)) (SUB1 N)))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(NOT (EQUAL (CAR U)
(NTH (CDR U) (SUB1 N))))).
Appealing to the lemma CAR/CDR.ELIM, we now replace U
by (CONS Z X) to eliminate (CDR U) and (CAR U). This
produces:
(IMPLIES (AND (EQUAL (INDEX X (NTH X (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH X) (SUB1 N)))
(NOT (MEMB Z X))
(ISPERM X)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1)))
(NOT (EQUAL Z (NTH X (SUB1 N))))),
which further simplifies, clearly, to:
(IMPLIES (AND (EQUAL (INDEX X (NTH X (SUB1 N)))
(SUB1 N))
(NOT (LESSP (LENGTH X) (SUB1 N)))
(NOT (MEMB (NTH X (SUB1 N)) X))
(ISPERM X)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL N 1)).
Appealing to the lemma SUB1.ELIM, replace N by
(ADD1 Z) to eliminate (SUB1 N). We rely upon the
type restriction lemma noted when SUB1 was introduced
to restrict the new variable. We thus obtain:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (INDEX X (NTH X Z)) Z)
(NOT (LESSP (LENGTH X) Z))
(NOT (MEMB (NTH X Z) X))
(ISPERM X)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (ADD1 Z) 1)).
However this simplifies further, rewriting with
ADD1.EQUAL, and expanding the definition of NUMBERP,
to:
(IMPLIES (AND (EQUAL (INDEX X (NTH X Z)) Z)
(NOT (LESSP (LENGTH X) Z))
(NOT (MEMB (NTH X Z) X))
(ISPERM X))
(EQUAL Z 0)).
We use the above equality hypothesis by substituting
(INDEX X (NTH X Z)) for Z and throwing away the
equality. This generates the new goal:
(IMPLIES
(AND (NOT (LESSP (LENGTH X)
(INDEX X (NTH X Z))))
(NOT (MEMB (NTH X (INDEX X (NTH X Z))) X))
(ISPERM X))
(EQUAL (INDEX X (NTH X Z)) 0)).
We will try to prove the above formula by
generalizing it, replacing (NTH X Z) by Y. We would
thus like to prove:
(IMPLIES
(AND (NOT (LESSP (LENGTH X) (INDEX X Y)))
(NOT (MEMB (NTH X (INDEX X Y)) X))
(ISPERM X))
(EQUAL (INDEX X Y) 0)),
which we generalize by replacing (INDEX X Y) by A.
We restrict the new variable by recalling the type
restriction lemma noted when INDEX was introduced.
This produces:
(IMPLIES (AND (NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
Finally give the above formula the name *1.1.
Case 1.2.
(IMPLIES (AND (EQUAL 0 (SUB1 N))
(NOT (LISTP U))
(NOT (LESSP 0 N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)).
But this simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND
(EQUAL (INDEX (CDR U) (NTH (CDR U) (SUB1 N)))
(SUB1 N))
(LISTP U)
(NOT (LESSP (ADD1 (LENGTH (CDR U))) N))
(NOT (MEMB (CAR U) (CDR U)))
(ISPERM (CDR U))
(NOT (EQUAL N 0))
(EQUAL N 1))
(EQUAL (INDEX U (CAR U)) N)),
which we again simplify, expanding NLISTP, INDEX, and
EQUAL, to:
T.
So we now return to:
(IMPLIES (AND (NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which is formula *1.1 above. Perhaps we can prove it by
induction. There are five plausible inductions. However,
they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP A)) (p A X))
(IMPLIES (EQUAL A 0) (p A X))
(IMPLIES (AND (NUMBERP A)
(NOT (EQUAL A 0))
(p (SUB1 A) (CDR X)))
(p A X))).
The inequality SUB1.LESSP establishes that the measure
(COUNT A) decreases according to the well-founded function
LESSP in the induction step of the scheme. Note, however,
the inductive instance chosen for X. The above induction
scheme leads to four new goals:
Case 4. (IMPLIES (AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
This simplifies, appealing to the lemmas CDR.NLISTP and
CAR.NLISTP, and opening up the definitions of NLISTP,
ISPERM, NTH, MEMB, LENGTH, EQUAL, and LESSP, to four new
formulas:
Case 4.4.
(IMPLIES
(AND (NOT (EQUAL (SUB1 A) 0))
(NUMBERP A)
(NOT (LISTP X))
(NOT (LESSP 0 A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 4.3.
(IMPLIES
(AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(NUMBERP A)
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL (SUB1 A) 0))
(NOT (LISTP X))
(NOT (LESSP 0 A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES
(AND (LESSP (LENGTH (CDR X)) (SUB1 A))
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which simplifies, applying CDR.NLISTP and CAR.NLISTP, and
opening up NLISTP, ISPERM, NTH, MEMB, LENGTH, EQUAL, and
LESSP, to two new goals:
Case 3.2.
(IMPLIES
(AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(NUMBERP A)
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(NOT (EQUAL A 1))
(NOT (MEMB (NTH (CDR X) (SUB1 A)) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)).
But this simplifies again, unfolding NLISTP and MEMB,
to:
T.
Case 3.1.
(IMPLIES
(AND (MEMB (NTH (CDR X) (SUB1 A)) (CDR X))
(LISTP X)
(NOT (LESSP (ADD1 (LENGTH (CDR X))) A))
(EQUAL A 1)
(NOT (MEMB (CAR X) X))
(NOT (MEMB (CAR X) (CDR X)))
(ISPERM (CDR X)))
(EQUAL A 0)),
which we again simplify, opening up EQUAL, NLISTP, and
MEMB, to:
T.
Case 2. (IMPLIES (AND (NOT (ISPERM (CDR X)))
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)),
which simplifies, rewriting with CDR.NLISTP and
CAR.NLISTP, and opening up the functions NLISTP, ISPERM,
NTH, MEMB, LENGTH, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (EQUAL (SUB1 A) 0)
(NUMBERP A)
(NOT (LESSP (LENGTH X) A))
(NOT (MEMB (NTH X A) X))
(ISPERM X))
(EQUAL A 0)).
Applying the lemma SUB1.ELIM, replace A by (ADD1 Z) to
eliminate (SUB1 A). We rely upon the type restriction
lemma noted when SUB1 was introduced to restrict the new
variable. This generates:
(IMPLIES (AND (NUMBERP Z)
(EQUAL Z 0)
(NOT (LESSP (LENGTH X) (ADD1 Z)))
(NOT (MEMB (NTH X (ADD1 Z)) X))
(ISPERM X))
(EQUAL (ADD1 Z) 0)),
which we simplify, unfolding the definitions of EQUAL,
NUMBERP, NTH, NLISTP, MEMB, LENGTH, and LESSP, to:
T.
That finishes the proof of *1.1, which, consequently,
finishes the proof of *1. Q.E.D.
[41960 cns / 228.3 s + 23.9 gc + 27.6 io (= 285 @ 1)]
FOO2
!
←DEFN(INVERT2 (U N M)
(IF (ZEROP N)
NIL
(CONS (INDEX U (ADD1 (DIFFERENCE M N)))
(INVERT2 U (SUB1 N) M))))
The lemma SUB1.LESSP establishes that (COUNT N) goes
down according to the well-founded function LESSP in each
recursive call. Hence, INVERT2 is accepted under the
definitional principle. Observe that:
(OR (LITATOM (INVERT2 U N M))
(LISTP (INVERT2 U N M)))
is a theorem.
[1779 cns / 6.8 s + 0.0 gc + .6 io (= 8 @ 1)]
INVERT2
!
←DEFN(INVERT (U)
(INVERT2 U (LENGTH U) (LENGTH U)))
Note that (OR (LITATOM (INVERT U)) (LISTP (INVERT U)))
is a theorem.
[568 cns / 2.6 s + 0.0 gc + .3 io (= 3 @ 1)]
INVERT
-------